Nuprl Lemma : iseg_transitivity2
4,23
postcript
pdf
T
:Type,
l1
,
l2
,
l3
:
T
List.
l2
l3
l1
l2
l1
l3
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
l1
l2
Lemmas
iseg
wf
,
iseg
transitivity
origin
T:Type, l1, l2, l3:T List. l2 
l3 
l1 l2 l1 l3 T:Type, l1, l2, l3:T List. l2 l3 l1 l2 l1 l3 Qx:A. B(x)
T l2